System F

For the electronic trance music artist, see Ferry Corsten.

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard and computer scientist John C. Reynolds.

Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A→ A would be formalized in System F as the judgment

$\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha$

where α is a type variable. The upper-case $\Lambda$ is traditionally used to denote type-level functions, as opposed to the lower-case $\lambda$ which is used for value-level functions.

As a term rewriting system, System F is strongly normalizing. Type inference in System F (without explicit type annotations) is undecidable however. Under the Curry–Howard isomorphism, System F corresponds to the fragment of second-order intuitionistic logic that uses only universal quantification. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types.

1 Logic and predicates
2 System F Structures
3 Use in programming languages
4 System F_ω
5 See also
6 References
7 Further reading
8 External links

Logic and predicates

The Boolean type is defined as: $\scriptstyle\forall\alpha.\alpha \to \alpha \to \alpha$ , where $\scriptstyle\alpha$ is a type variable. This produces the following two definitions for the boolean values $\scriptstyle\mathbf{T}$ and $\scriptstyle\mathbf{F}$ :

$\mathbf{T} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^\alpha{.}x$

$\mathbf{F} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^{\alpha}{.}y$

Then, with these two $\scriptstyle\lambda$ -terms, we can define some logic operators:

$\mathrm{AND} = \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x\, \mathsf{Boolean}\, y\, \mathbf{F}$

$\mathrm{OR} = \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x\, \mathsf{Boolean}\, \mathbf{T}\, y$

$\mathrm{NOT} = \lambda x^{\mathsf{Boolean}}{.} x\, \mathsf{Boolean}\, \mathbf{F}\, \mathbf{T}$

There is no need for an IFTHENELSE function as one can just use raw $\scriptstyle\mathsf{Boolean}$ -typed terms as decision functions. However, if one is requested:

$\mathrm{IFTHENELSE} = \Lambda \alpha.\lambda x^{\mathsf{Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}. x \alpha y z$

will do. A predicate is a function which returns a $\scriptstyle\mathsf{Boolean}$ -typed value. The most fundamental predicate is ISZERO which returns $\scriptstyle\mathbf{T}$ if and only if its argument is the Church numeral 0:

$\mathrm{ISZERO} = \lambda n^{\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha}{.}n\, \mathsf{Boolean}\, (\lambda x^\mathsf{Boolean}{.}\mathbf{F})\, \mathbf{T}$

System F Structures

System F allows recursive constructions to be embedded in a natural manner, related to that in Martin-Löf's type theory. Abstract structures (S) are created using constructors. These are functions typed as:

$K_1\rightarrow K_2\rightarrow\dots\rightarrow S$ .

Recursivity is manifested when $S$ itself appears within one of the types $K_i$ . If you have $m$ of these constructors, you can define the type of $S$ as:

$\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha$

For instance, the natural numbers can be defined as an inductive datatype $N$ with constructors

$\mathit{zero}�: \mathrm{N}$

$\mathit{succ}�: \mathrm{N} \rightarrow \mathrm{N}$

The System F type corresponding to this structure is $\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha$ . The terms of this type comprise a typed version of the Church numerals, the first few of which are:

0 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x$

1 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x$

2 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)$

3 := $\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))$

If we reverse the order of the curried arguments (i.e., $\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha$ ), then the Church numeral for $n$ is a function that takes a function f as argument and returns the $n$ ^th power of f. That is to say, a Church numeral is a higher-order function – it takes a single-argument function f, and returns another single-argument function.

Use in programming languages

The version of System F used in this article is as an explicitly typed, or Church-style, calculus. The typing information contained in λ-terms makes type-checking straightforward. Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking is undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations. ^[1]^[2]

Wells' result implies that type inference for System F is impossible. A restriction of System F known as "Hindley–Milner", or simply "HM", does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell 98 and ML. Over time, as the restrictions of HM-style type systems have become apparent, languages have steadily moved to more expressive logics for their type systems. As of 2008, GHC, a Haskell compiler, goes beyond HM, and now uses System F extended with non-syntactic type equality, for example.

System F_ω

Although System F corresponds to the first axis of the Barendregt's lambda cube, system F_ω combines the first axis (polymorphism) with type operators (the second axis); it is a different, more complex system.

System F_ω can be defined inductively on a family of systems, where induction is based on the kinds permitted in each system:

permits kinds:
- $\star$ (the kind of types) and
- $J\Rightarrow K$ where $J\in F_{n-1}$ and $K\in F_n$ (the kind of functions from types to types, where the argument type is of a lower order)

In the limit, we can define system $F_\omega$ to be

$F_\omega = \underset{1 \leq i}{\bigcup} F_i$

That is, F_ω is the system which allows functions from types to types where the argument (and result) may be of any order.

Note that although F_ω places no restrictions on the order of the arguments in these mappings, it does restrict the universe of the arguments for these mappings: they must be types rather than values. System F_ω does not permit mappings from values to types (Dependent types), though it does permit mappings from values to values ( $\lambda$ abstraction), mappings from types to values ( $\Lambda$ abstraction, sometimes written $\forall$ ) and mappings from types to types ( $\lambda$ abstraction at the level of types)

References

Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Proceedings of the Second Scandinavian Logic Symposium. Amsterdam. pp. 63–92.
Reynolds, John (1974). "Towards a Theory of Type Structure". Colloque sur la Programmation. Paris, France. pp. 408–425. ftp://ftp.cs.cmu.edu/user/jcr/theotypestr.pdf. Retrieved 6 Apr 2010.
Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0 521 37181 3.
J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. [1]

External links

Summary of System F by Franck Binard.

System F

Contents

Logic and predicates

System F Structures

Use in programming languages

System Fω

See also

References

Further reading

External links

System F_ω